Nuprl Lemma : es-interface-conditional-domain
11,40
postcript
pdf
es
:ES,
A
:Type,
I1
,
I2
:AbsInterface(
A
),
e
:E. (
e
[
I1
?
I2
]) = ((
e
I1
)
(
e
I2
))
latex
Definitions
can-apply(
f
;
x
)
,
e
X
,
[
f
?
g
]
,
p
q
,
<
a
,
b
>
,
,
s
=
t
,
E
,
x
:
A
.
B
(
x
)
,
AbsInterface(
A
)
,
Type
,
ES
,
t
T
,
x
:
A
B
(
x
)
,
Top
,
left
+
right
,
x
:
A
B
(
x
)
,
b
,
t
.1
,
False
,
A
,
if
b
then
t
else
f
fi
,
tt
,
P
Q
,
P
&
Q
,
P
Q
,
Unit
,
f
(
a
)
,
isl(
x
)
,
P
Q
Lemmas
eqtt
to
assert
,
iff
transitivity
,
eqff
to
assert
,
assert
of
bnot
,
isl
wf
origin
es:ES, A:Type, I1, I2:AbsInterface(A), e:E. (e 
[I1?I2]) = ((e I1) 
(e I2)) 
es:ES, A:Type, I1, I2:AbsInterface(A), e:E. (e [I1?I2]) = ((e I1) (e I2)) Xqx:A. B(x) T
B(x)
B(x)
b
A
Q
Q Q